<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD>



<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<META name="GENERATOR" content="hevea 1.08">
<LINK rel="stylesheet" type="text/css" href="libman.css">
<TITLE>
Introduction
</TITLE>
</HEAD>
<BODY >
<A HREF="libman042.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="libman044.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
<HR>

<H2 CLASS="section"><A NAME="htoc80">8.1</A>&nbsp;&nbsp;Introduction</H2>
<EM>Constraint handling rules</EM> (<FONT COLOR=purple>CHR</FONT>s,
CHR home page <A HREF="http://www.cs.kuleuven.ac.be/~dtai/projects/CHR/"><TT>http://www.cs.kuleuven.ac.be/~dtai/projects/CHR/</TT></A>)
[<A HREF="libman072.html#fru92"><CITE>6</CITE></A>]
are a high-level language
extension to write <EM>user-defined</EM> constraints. <FONT COLOR=purple>CHR</FONT>s 
consists of guarded rules with multiple heads.
<BR>
<BR>
The high-level <FONT COLOR=purple>CHR</FONT>s are an excellent tool for <EM>rapid prototyping</EM> and
implementation of constraint handlers. The usual abstract formalism to
describe a constraint system, i.e. inference rules, rewrite rules,
sequents, formulas expressing axioms and theorems, can be written as
<FONT COLOR=purple>CHR</FONT>s in a straightforward way. Starting from this <EM>executable
specification</EM>, the rules can be refined and adapted
to the specifics of the application. <BR>
<BR>
<FONT COLOR=purple>CHR</FONT>s define <EM>simplification</EM> of, and <EM>propagation</EM> over, 
user-defined constraints. Simplification replaces constraints by
simpler constraints while preserving logical equivalence (e.g. <TT>X&gt;Y,Y&gt;X
&lt;=&gt; fail</TT>). Propagation adds new constraints which are logically
redundant but may cause further simplification (e.g. <TT>X&gt;Y,Y&gt;Z ==&gt; X&gt;Z</TT>). Repeatedly applying <FONT COLOR=purple>CHR</FONT>s incrementally simplifies and
finally solves user-defined constraints (e.g. <TT>A&gt;B,B&gt;C,C&gt;A</TT>
leads to <TT>fail</TT>). <BR>
<BR>
With multiple heads and propagation rules,
<FONT COLOR=purple>CHR</FONT>s provide two features which are essential for non-trivial
constraint handling.
The declarative reading of
<FONT COLOR=purple>CHR</FONT>s as formulas of first order logic 
allows one to reason about their correctness. On the other hand, 
regarding <FONT COLOR=purple>CHR</FONT>s as a rewrite system on logical formulas allows one to
reason about their termination and confluence.<BR>
<BR>
In the next section
it is explained how to use <FONT COLOR=purple>CHR</FONT>s.
 Then,
example constraint handlers and the colour graphic
demo are listed.
 The next
section introduces the basics of the <FONT COLOR=purple>CHR</FONT> language and how it works. 
The next section describes more of the <FONT COLOR=purple>CHR</FONT> language,
the section after the built-in labeling feature.
Then there is
a section on how to write good <FONT COLOR=purple>CHR</FONT> programs. Next the debuggers for
<FONT COLOR=purple>CHR</FONT>s are introduced. 
<BR>
<BR>
<HR>
<A HREF="libman042.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="libman044.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
</BODY>
</HTML>
